T:Type, L:(T List), R:({x:T| (x  L)} es_realizer{i:l}), A:es_realizer{i:l}.
R-compat{i:l}(A; Rall(L; x.R(x)))  (x:T. (x  L)  R-compat{i:l}(A; R(x))) 

latex

Definitions	ff, tt, i <z j, b, i z j, if b then t else f fi , nth_tl(n;as), hd(l), lelt(i; j; k), Y, ||as||, int_seg(i; j), l[i], False, A, A  B, A c B, x:A. B(x), guard(T), P  Q, (x  l), prop{i:l}, P  Q, P  Q, x. t(x), top, P  Q, x(s), P  Q, t  T, x:A. B(x),
Lemmas	and functionality wrt iff, R-compat-Rplus2, Rall wf, Rplus wf, iff functionality wrt iff, non neg length, select member, Rall-cons, subtype rel self, select wf, length wf1, nat wf, cons member, subtype rel function, R-compat-none, R-compat-symmetry, nil member, es realizer wf, Rnone wf, R-compat wf, l member wf, Rall-nil